////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the implementation of the KeyInput wrapper.
///

#include "keyinput.hpp"

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include <boost/foreach.hpp>
#define foreach BOOST_FOREACH

#include <boost/algorithm/string/replace.hpp>
using boost::replace_all;

#include <boost/tokenizer.hpp>

#include <cctype>

#include "common/assert.hpp"
#include "common/ptr.hpp"
#include "common/string.hpp"
#include "codestream.hpp"
#include "exclusivevisitor.hpp"
#include "findreferences.hpp"
#include "nodes.hpp"
#include "operator.hpp"
#include "parse.hpp"
#include "tree.hpp"

////////////////////////////////////////////////////////////////////////////////
// KeyVisitor Class                                                           //
////////////////////////////////////////////////////////////////////////////////

/// Visits the nodes of an abstract syntax tree to translate expressions to KeY,
/// to a stream. A visitor in the visitor pattern.
///
class KeyVisitor : public ExclusiveVisitor {
	public:
		
		/// Construct an KeY visitor.
		///
		KeyVisitor(
			ostream& o ///< the stream to send the key code to
		);
		
		VISIT_FUNCTIONS_FROM(
			(OperatorCall)
			(FunctionCall)
			(Reference)
			(BooleanLiteral)
			(IntegerLiteral)
			(ChainExpression)
			(ArrayType)
			(NamedType)
		)
	
	private:
		
		/// \return the ordinal of the parameter name in the function from 1
		///         0, if there is no such parameter
		///
		uint parameter_index(wptr<FunctionDeclaration> decl, string param);
		
		void recursive_composite_operator(wptr<Operator> op, vector<wptr<Expression> > operands, wptr<Symbol> scope, vector<wptr<Reference> > references, uint compositeIndex = 0);
		
		ostream& out;
};

////////////////////////////////////////////////////////////////////////////////
// Function Implementations                                                   //
////////////////////////////////////////////////////////////////////////////////

KeyInput::KeyInput(wptr<Expression> expr) : _expression(expr) {
	assert(expr);
}

ostream& KeyInput::send_to_stream(ostream& out) const {
	sptr<KeyVisitor> visitor(new KeyVisitor(out));
	
	set<wptr<Symbol> > referencesUsed = find_references(_expression);
	
	foreach (wptr<Symbol> ref, referencesUsed)
		if (typeid(*ref->type) == typeid(FunctionType))
			referencesUsed.erase(ref);
	
	if (!referencesUsed.empty()) {
		out << "\\programVariables {\n";
		foreach (wptr<Symbol> symbol, referencesUsed) {
			out << "\t";
			symbol->type->accept(visitor);
			out << " " << symbol->unique_name() << ";\n";
		}
		out << "}\n\n";
	}
	
	out << "\\problem {\n\t";
	_expression->accept(visitor);
	out << "\n}\n";
	
	return out;
}

////////////////////////////////////////////////////////////////////////////////

KeyVisitor::KeyVisitor(ostream& o) : out(o) {
} // intentionally empty

uint KeyVisitor::parameter_index(wptr<FunctionDeclaration> decl, string param) {
	uint i = 1;
	foreach (wptr<Identifier> id, decl->parameterNames) {
		if (id->text == param)
			return i;
		++i;
	}
	return 0;
}

void KeyVisitor::recursive_composite_operator(wptr<Operator> op, vector<wptr<Expression> > operands, wptr<Symbol> scope, vector<wptr<Reference> > references, uint compositeIndex) {
	wptr<SingleOperator> sop;
	
	sptr<Reference> ref = references[compositeIndex];
	assert(ref->symbol()->declaration);
	assert(typeid(*ref->symbol()->declaration) == typeid(FunctionDeclaration));
	assert(!ref->symbol()->declaration.cast<FunctionDeclaration>()->KeY.empty());
	
	string nonWordChars;
	for (char c = 1; 1 <= c && c <= 127; ++c) // may use wrap-around for test
		if (!isalnum(c) && c != '_')
			nonWordChars.push_back(c);
	
	boost::char_separator<char> sep("", nonWordChars.c_str());
	boost::tokenizer<boost::char_separator<char> > tokens(*ref->symbol()->declaration->KeY.begin(), sep);
	foreach (string token, tokens) {
		uint index = parameter_index(ref->symbol()->declaration, token);
		if (index) {
			if (typeid(*op) == typeid(CompositeOperator) && compositeIndex < op.cast<CompositeOperator>()->operators().size() - 1) {
				recursive_composite_operator(op, operands, scope, references, compositeIndex + 1);
			} else {
				operands[index-1]->accept(wptr_this());
			}
		} else {
			out << token;
		}
	}
}

void KeyVisitor::visit(wptr<OperatorCall> node) {
	assert(node);
	
	bool addTRUE = (
		   typeid(*node->op) == typeid(SingleOperator)
		&& node->op.cast<SingleOperator>()->function_name() == "subscript"
		&& same_type(node->operands[0]->type().cast<ArrayType>()->type, parse<Type>(".bool", node->scope()))
	);
	
	vector<sptr<Reference> > references = get_operator_references(node->op, weak_vector(node->operands), node->scope());
	
	if (addTRUE) out << "(";
	recursive_composite_operator(node->op, weak_vector(node->operands), node->scope(), weak_vector(references));
	if (addTRUE) out << " = TRUE)";
}

void KeyVisitor::visit(wptr<FunctionCall> node) {
	assert(node);
	
	assert(typeid(*node->base) == typeid(Reference));
	assert(node->base.cast<Reference>()->symbol()->declaration);
	assert(!node->base.cast<Reference>()->symbol()->declaration->KeY.empty());
	
	string nonWordChars;
	for (char c = 1; 1 <= c && c <= 127; ++c) // may use wrap-around for test
		if (!isalnum(c) && c != '_')
			nonWordChars.push_back(c);
	
	boost::char_separator<char> sep("", nonWordChars.c_str());
	boost::tokenizer<boost::char_separator<char> > tokens(*node->base.cast<Reference>()->symbol()->declaration->KeY.begin(), sep);
	foreach (string token, tokens) {
		uint index = parameter_index(node->base.cast<Reference>()->symbol()->declaration, token);
		if (index) {
			node->parameters[index-1]->accept(wptr_this());
		} else {
			out << token;
		}
	}
}

void KeyVisitor::visit(wptr<Reference> node) {
	assert(node);
	
	bool addTRUE = same_type(node->type(), parse<Type>(".bool", node->scope()));
	
	if (addTRUE) out << "(";
	out << node->symbol()->unique_name();
	if (addTRUE) out << " = TRUE)";
}

void KeyVisitor::visit(wptr<BooleanLiteral> node) {
	assert(node);
	
	out << (node->value ? "true" : "false");
}

void KeyVisitor::visit(wptr<IntegerLiteral> node) {
	assert(node);
	
	out << node->value;
}

void KeyVisitor::visit(wptr<ChainExpression> node) {
	assert(node);
	
	out << "(";
	for (uint i = 0; i < node->operators.size(); ++i) {
		if (i > 0) out << " & ";
		vector<wptr<Expression> > operands;
		operands.push_back(node->operands[i]);
		operands.push_back(node->operands[i+1]);
		vector<sptr<Reference> > references = get_operator_references(node->operators[i], operands, node->scope());
		recursive_composite_operator(node->operators[i], operands, node->scope(), weak_vector(references));
	}
	out << ")";
}

void KeyVisitor::visit(wptr<ArrayType> node) {
	assert(node);
	
	node->type->accept(wptr_this());
	out << "[]";
}

void KeyVisitor::visit(wptr<NamedType> node) {
	assert(node);
	
	out << node->reference->symbol()->typeDeclaration->KeY;
}
